(*
** Definiciones y lemas sobre logica de Hoare.
** Lemas utiles para la demostracion principal en MiniAesInv.v.
*)

Require Import TypesImpl.
Open Scope Z_scope.
Open Scope lang_scope.
Require Import Matrix.


Definition Assertion := State -> Prop.

Definition hoare_triple
           (P:Assertion)(instr:Instr)(Q:Assertion) : Prop :=
  forall st st', st $ instr => st' -> P st -> Q st'.

Notation "{{ P }} c {{ Q }}" :=
  (hoare_triple P c Q) (at level 90, c at next level).

Definition assn_sub X a (P: Assertion) : Assertion :=
  fun (st : State) =>
    forall n, ByteEval st a (Some n) -> P (update st X (byte_val n)).

Definition matrix_set_sub (mid: Id)(i j: Z)(b: ByteExp)(P: Assertion) : Assertion :=
  fun st:State =>
    forall m n (matr matr': Matrix Byte m n) i0 j0 b0, ArithEval st i i0 -> ArithEval st j j0 -> ByteEval st b (Some b0) -> MatrixEval st mid matr -> matrix_set Byte m n matr i0 j0 b0 = Some matr' -> P (update st mid (byte_matrix_val matr')).

Notation "P [ X |-> a ]" := (assn_sub X a P) (at level 10). 

Theorem hoare_asgn : forall Q X a,
  {{Q [X |-> a]}} (byte X ::= a) {{Q}}.
Proof.
  unfold hoare_triple.
  intros Q X a st st' HE HQ.
  inversion HE. subst.
  unfold assn_sub in HQ.
apply HQ. assumption. Qed.

Theorem hoare_seq : forall P Q R c1 c2,
     {{P}} c1 {{Q}} ->
     {{Q}} c2 {{R}} ->
     {{P}} c1;c2 {{R}}.
Proof.
  intros P Q R c1 c2 H1 H2 st st' H12 Pre.
  inversion H12; subst.
  apply (H2 st'0 st'). try assumption.
  apply (H1 st st'0); assumption. Qed.

Definition assert_implies (P Q : Assertion) : Prop :=
  forall st, P st -> Q st.

Notation "P ->> Q" :=
  (assert_implies P Q) (at level 80) : hoare_spec_scope.
Open Scope hoare_spec_scope.

Theorem hoare_consequence_pre : forall (P P' Q : Assertion) c,
  {{P'}} c {{Q}} ->
  P ->> P' ->
  {{P}} c {{Q}}.
Proof.
  intros P P' Q c Hhoare Himp.
  intros st st' Hc HP. apply (Hhoare st st').
  assumption. apply Himp. assumption. Qed.

Theorem hoare_consequence_post : forall(P Q Q' : Assertion) c,
  {{P}} c {{Q'}} ->
  Q' ->> Q ->
  {{P}} c {{Q}}.
Proof.
  intros P Q Q' c Hhoare Himp.
  intros st st' Hc HP.
  apply Himp.
  apply (Hhoare st st').
  assumption. assumption. Qed.

Definition bassn b : Assertion :=
  fun st => st b = Some (bool_val true).

Lemma bexp_eval_true : forall b st,
  st b = Some (bool_val true) -> (bassn b) st.
Proof.
intros.
unfold bassn.
assumption.
Qed.

Lemma bexp_eval_false : forall b st,
  st b = Some (bool_val false) -> ~ ((bassn b) st).
Proof.
  intros b st Hbe contra.
  unfold bassn in contra.
  rewrite contra in Hbe. inversion Hbe.
Qed.

Theorem hoare_if : forall P Q b c1 c2,
  {{fun st => P st /\ bassn b st}} c1 {{Q}} ->
  {{fun st => P st /\ ~(bassn b st)}} c2 {{Q}} ->
  {{P}} (IFB bool_exp_id b THEN c1 ELSE c2 END) {{Q}}.
Proof.
  intros P Q b c1 c2 HTrue HFalse st st' HE HP.
  inversion HE; subst.
    apply (HTrue st st').
      assumption.
      split. assumption.
             apply bexp_eval_true. inversion_clear H3. assumption.
    apply (HFalse st st').
      assumption.
      split. assumption.
             apply bexp_eval_false. inversion_clear H3. assumption.
Qed.

Require String. Open Scope string_scope.

Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.

Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.

Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].

Tactic Notation "ceval_cases" tactic(first) :=
  first.

Tactic Notation "Case" constr(name) := Case_aux Case name.

Lemma hoare_while : forall P b c,
  {{fun st => P st /\ bassn b st}} c {{P}} ->
  {{P}} WHILE (bool_exp_id b) DO c END {{fun st => P st /\ ~ (bassn b st)}}.
Proof.
  intros P b c Hhoare st st' He HP.
  remember (WHILE (bool_exp_id b) DO c END) as wcom eqn:Heqwcom.
  induction He;
    try (inversion Heqwcom); subst; clear Heqwcom.
    apply IHHe2. reflexivity. unfold hoare_triple in Hhoare. apply (Hhoare st st'). assumption.
    split. assumption. apply bexp_eval_true. inversion H. assumption.

    split. assumption.
    apply bexp_eval_false.
    inversion H. assumption.
Qed.

Lemma hoare_for : forall P (i: Id) n c,
  {{fun st => P st /\ BoolEval st (i lt n) TRUE}} c {{P}} ->
  {{P}} FOR i TO n DO c END {{fun st => P st /\ BoolEval st (i ge n) TRUE}}.
Proof.
  intros P i n c Hhoare st st' He HP.
  remember (FOR i TO n DO c END) as wcom eqn:Heqwcom.
  induction He;
    try (inversion Heqwcom); subst; clear Heqwcom.
    split; assumption.
    apply IHHe2. reflexivity. unfold hoare_triple in Hhoare. apply (Hhoare st st'). assumption.
    split; assumption.
Qed.

Theorem hoare_matrix_set : forall Q (mid: Id)(i j: Z) b,
  {{ (matrix_set_sub mid i j b Q) }} instr_matrix_set mid i j b {{ Q }}.
Proof.
  unfold hoare_triple.
  intros.
  inversion_clear H.
  unfold matrix_set_sub in H0.
  eapply H0.
  apply H2.
  apply H3.
  apply H4.
  apply H1.
  apply H5.
Qed.

Theorem hoare_xor : forall X (b1 b2: Byte),
  {{ fun st => st X = Some (byte_val b1) }}
      byte X ::= byte_exp_xor X b2
  {{ fun st => st X = Some (byte_val (byte_xor b1 b2)) }}.
Proof.
intros.
eapply hoare_consequence_pre.
apply hoare_asgn.
intros st1 H0 bxor3 H2.
unfold update.
destruct (equal_id X X) eqn:?.
inversion_clear H2.
inversion_clear H1.
inversion_clear H in H0.
rewrite H1 in H0.
inversion H0.
rewrite <- H2.
reflexivity.
destruct X.
unfold equal_id in *.
elim (beq_nat_false n n); auto.
Qed.

Theorem xor_inverse : forall x key, Z.lxor (Z.lxor x key) key = x.
intros.
destruct x.
destruct key.
apply Z.lxor_0_l.
apply Z.lxor_nilpotent.
rewrite Z.lxor_assoc.
rewrite Z.lxor_nilpotent.
apply Z.lxor_0_r.
rewrite Z.lxor_assoc.
rewrite Z.lxor_nilpotent.
apply Z.lxor_0_r.
rewrite Z.lxor_assoc.
rewrite Z.lxor_nilpotent.
apply Z.lxor_0_r.
Qed.

Theorem nibble_xor : forall a b,
  0 <= a < 16 -> 0 <= b < 16 -> 0 <= Z.lxor a b < 16.
Proof.
  intros.
  destruct a; destruct b; auto.
  try (inversion H; elim H1; auto; fail);
  destruct p; try destruct p;
    try destruct p; try destruct p;
    try destruct p;
    try (inversion H; inversion H2; fail);
    try (inversion H; elim H1; auto; fail);
  destruct p0; try destruct p0;
    try destruct p0; try destruct p0;
    try destruct p0;
    try (inversion H0; inversion H2; fail); simpl; omega.
  inversion H; elim H1; auto.
Qed.

Theorem get_some : forall m n i j (matr: Matrix Byte m n),
  m >= 1 -> n >= 1 -> 0 <= i < m -> 0 <= j < n -> exists b, matrix_get Byte m n i j matr = Some b.
Proof.
intros.
apply Matrix.get_some.
replace 1%nat with (Z.to_nat 1).
apply Z2Nat.inj_le; omega.
auto.
replace 1%nat with (Z.to_nat 1).
apply Z2Nat.inj_le; omega.
auto.
split.
replace 0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
split.
replace 0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
Qed.

Theorem set_matrix : forall i j m n (matr: Matrix Byte m n) b,
  0 <= i < m -> 0 <= j < n -> exists matr', matrix_set Byte m n matr i j b = Some matr'.
Proof.
intros.
apply Matrix.set_matrix.
split.
replace 0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
split.
replace 0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
Qed.


Definition matrix_defined (matr: Matrix Byte 2 2)(m00 m01 m10 m11: Byte) :=
  matrix_get Byte 2 2 0 0 matr = Some m00 /\
  matrix_get Byte 2 2 0 1 matr = Some m01 /\
  matrix_get Byte 2 2 1 0 matr = Some m10 /\
  matrix_get Byte 2 2 1 1 matr = Some m11
.


Theorem set_matrix_get : forall i j m n (matr matr': Matrix Byte m n) b,
                        m >= 1 -> 0 <= i < m ->  n >= 1 -> 0 <= j < n ->
                        matrix_set Byte m n matr i j b = Some matr' ->
                        matrix_get Byte m n i j matr' = Some b.
Proof.
intros.
apply (Matrix.set_matrix_get matr).
replace  1%nat with (Z.to_nat 1).
apply Z2Nat.inj_le; omega.
auto.
split.
replace  0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
replace  1%nat with (Z.to_nat 1).
apply Z2Nat.inj_le; omega.
auto.
split.
replace  0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
auto.
Qed.

Theorem get_set_other_matrix_get : forall i j q s m n (matr matr': Matrix Byte m n) a b,
                        0 <= i < m -> 0 <= j < n ->
                        0 <= q < m -> 0 <= s < n ->
                        ~ ((i = q) /\ (j = s)) ->
                        matrix_get Byte m n i j matr = Some a ->
                        matrix_set Byte m n matr q s b = Some matr' ->
                        matrix_get Byte m n i j matr' = Some a.
Proof.
intros.
eapply (Matrix.get_set_other_matrix_get matr).
split.
replace  0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
split.
replace  0%nat with (Z.to_nat 0).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
split.
replace  0%nat with (Z.to_nat 0).
instantiate (1:=Z.to_nat q).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
split.
replace  0%nat with (Z.to_nat 0).
instantiate (1:=Z.to_nat s).
apply Z2Nat.inj_le; omega.
auto.
apply Z2Nat.inj_lt; omega.
unfold not.
intros.
absurd  (i = q /\ j = s).
assumption.
split.
apply Z2Nat.inj.
omega.
omega.
apply H6.
apply Z2Nat.inj.
omega.
omega.
apply H6.
auto.
instantiate (1:=b).
auto.
Qed.



Lemma matrix_get_set_00 : forall matr matr' m00 m01 m10 m11 b,
  matrix_defined matr m00 m01 m10 m11 ->
  matrix_set Byte 2 2 matr 0 0 b = Some matr' -> matrix_defined matr' b m01 m10 m11.
Proof.
unfold matrix_defined.
intros.
split.
apply (set_matrix_get  0 0 2 2 matr).
omega.
omega.
omega.
split.
omega.
omega.
assumption.
split.
apply (get_set_other_matrix_get 0 1 0 0 2 2 matr matr' m01 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
split.
apply (get_set_other_matrix_get 1 0 0 0 2 2 matr matr' m10 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
apply (get_set_other_matrix_get 1 1 0 0 2 2 matr matr' m11 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
Qed.


Lemma matrix_get_set_01 : forall matr matr' m00 m01 m10 m11 b,
  matrix_defined matr m00 m01 m10 m11 ->
  matrix_set Byte 2 2 matr 0 1 b = Some matr' -> matrix_defined matr' m00 b m10 m11.
Proof.
unfold matrix_defined.
intros.
split.
apply (get_set_other_matrix_get 0 0 0 1 2 2 matr matr' m00 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.

split.
apply (set_matrix_get  0 1 2 2 matr).
omega.
omega.
omega.
split.
omega.
omega.
assumption.



split.
apply (get_set_other_matrix_get 1 0 0 1 2 2 matr matr' m10 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
apply (get_set_other_matrix_get 1 1 0 1 2 2 matr matr' m11 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
Qed.

Lemma matrix_get_set_10 : forall matr matr' m00 m01 m10 m11 b,
  matrix_defined matr m00 m01 m10 m11 ->
  matrix_set Byte 2 2 matr 1 0 b = Some matr' -> matrix_defined matr' m00 m01 b m11.
Proof.
unfold matrix_defined.
intros.
split.
apply (get_set_other_matrix_get 0 0 1 0 2 2 matr matr' m00 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
split.
apply (get_set_other_matrix_get 0 1 1 0 2 2 matr matr' m01 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
split.
apply (set_matrix_get  1 0 2 2 matr).
omega.
omega.
omega.
split.
omega.
omega.
assumption.
apply (get_set_other_matrix_get 1 1 1 0 2 2 matr matr' m11 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
Qed.

Lemma matrix_get_set_11 : forall matr matr' m00 m01 m10 m11 b,
  matrix_defined matr m00 m01 m10 m11 ->
  matrix_set Byte 2 2 matr 1 1 b = Some matr' -> matrix_defined matr' m00 m01 m10 b.
Proof.
unfold matrix_defined.
intros.
split.
apply (get_set_other_matrix_get 0 0 1 1 2 2 matr matr' m00 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
split.
apply (get_set_other_matrix_get 0 1 1 1 2 2 matr matr' m01 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
split.
apply (get_set_other_matrix_get 1 0 1 1 2 2 matr matr' m10 b).
omega.
omega.
omega.
omega.
omega.
apply H.
apply H0.
apply (set_matrix_get  1 1 2 2 matr).
omega.
omega.
omega.
split.
omega.
omega.
assumption.
Qed.

Lemma equals : forall b key, Some (byte_val b) = Some (byte_val (byte_xor (byte_xor b key) key)).
Proof.
intros.
replace (byte_xor (byte_xor b key) key) with b.
auto.
unfold byte_xor.
symmetry.
apply xor_inverse.
Qed.



Lemma matrix_some_eq :
  forall n m (mat1 mat2:Matrix Byte n m),
  Some (byte_matrix_val mat1) = Some (byte_matrix_val mat2) ->
  mat1 = mat2.
Proof.
  Hint Resolve Z_eq_dec.
  intros.
  assert (byte_matrix_val mat1 = byte_matrix_val mat2).
  remember (byte_matrix_val mat1).
  remember (byte_matrix_val mat2).
  clear Heqv Heqv0.
  injection H. auto.
  clear H.
  injection H0; intros; clear H0.

  match goal with
    |[H: existT ?P ?A ?x = existT ?P ?A ?x' |-_] =>
     remember x; remember x'
  end.
  assert (s = s0).
  rewrite <- EqdepFacts.eq_sigT_snd with (x1:=n) (H1:=s) (H:=H); eauto.
  apply Eqdep_dec.eq_rect_eq_dec with (A:=Integer)
    (Q:=fun m0 : Integer => {n0 : Integer & Matrix Byte m0 n0}) (x:=s); auto.

  subst s0.
  rewrite Heqs in H0.
  clear dependent s.
  rewrite <- EqdepFacts.eq_sigT_snd with (x1:=m) (H1:=mat1) (H:=H0); eauto.
  apply Eqdep_dec.eq_rect_eq_dec; auto.
Qed.

Definition sbox_defined (miniSbox: Matrix Byte 1 16) :=
    matrix_get Byte 1 16 0 0 miniSbox = Some 14 /\
    matrix_get Byte 1 16 0 1 miniSbox = Some 4 /\
    matrix_get Byte 1 16 0 2 miniSbox = Some 13 /\
    matrix_get Byte 1 16 0 3 miniSbox = Some 1 /\
    matrix_get Byte 1 16 0 4 miniSbox = Some 2 /\
    matrix_get Byte 1 16 0 5 miniSbox = Some 15 /\
    matrix_get Byte 1 16 0 6 miniSbox = Some 11 /\
    matrix_get Byte 1 16 0 7 miniSbox = Some 8 /\
    matrix_get Byte 1 16 0 8 miniSbox = Some 3 /\
    matrix_get Byte 1 16 0 9 miniSbox = Some 10 /\
    matrix_get Byte 1 16 0 10 miniSbox = Some 6 /\
    matrix_get Byte 1 16 0 11 miniSbox = Some 12 /\
    matrix_get Byte 1 16 0 12 miniSbox = Some 5 /\
    matrix_get Byte 1 16 0 13 miniSbox = Some 9 /\
    matrix_get Byte 1 16 0 14 miniSbox = Some 0 /\
    matrix_get Byte 1 16 0 15 miniSbox = Some 7
.

Definition sbox_inv_defined (miniSbox: Matrix Byte 1 16) :=
    matrix_get Byte 1 16 0 0 miniSbox = Some 14 /\
    matrix_get Byte 1 16 0 1 miniSbox = Some 3 /\
    matrix_get Byte 1 16 0 2 miniSbox = Some 4 /\
    matrix_get Byte 1 16 0 3 miniSbox = Some 8 /\
    matrix_get Byte 1 16 0 4 miniSbox = Some 1 /\
    matrix_get Byte 1 16 0 5 miniSbox = Some 12 /\
    matrix_get Byte 1 16 0 6 miniSbox = Some 10 /\
    matrix_get Byte 1 16 0 7 miniSbox = Some 15 /\
    matrix_get Byte 1 16 0 8 miniSbox = Some 7 /\
    matrix_get Byte 1 16 0 9 miniSbox = Some 13 /\
    matrix_get Byte 1 16 0 10 miniSbox = Some 9 /\
    matrix_get Byte 1 16 0 11 miniSbox = Some 6 /\
    matrix_get Byte 1 16 0 12 miniSbox = Some 11 /\
    matrix_get Byte 1 16 0 13 miniSbox = Some 2 /\
    matrix_get Byte 1 16 0 14 miniSbox = Some 0 /\
    matrix_get Byte 1 16 0 15 miniSbox = Some 5
.

Definition mult_table_defined (multTable: Matrix Byte 16 16) :=
  matrix_get Byte 16 16 0 0 multTable = Some 0 /\
  matrix_get Byte 16 16 0 1 multTable = Some 3 /\
  matrix_get Byte 16 16 0 2 multTable = Some 6 /\
  matrix_get Byte 16 16 0 3 multTable = Some 5 /\
  matrix_get Byte 16 16 0 4 multTable = Some 12 /\
  matrix_get Byte 16 16 0 5 multTable = Some 15 /\
  matrix_get Byte 16 16 0 6 multTable = Some 10 /\
  matrix_get Byte 16 16 0 7 multTable = Some 9 /\
  matrix_get Byte 16 16 0 8 multTable = Some 11 /\
  matrix_get Byte 16 16 0 9 multTable = Some 8 /\
  matrix_get Byte 16 16 0 10 multTable = Some 13 /\
  matrix_get Byte 16 16 0 11 multTable = Some 14 /\
  matrix_get Byte 16 16 0 12 multTable = Some 7 /\
  matrix_get Byte 16 16 0 13 multTable = Some 4 /\
  matrix_get Byte 16 16 0 14 multTable = Some 1 /\
  matrix_get Byte 16 16 0 15 multTable = Some 2 /\
  matrix_get Byte 16 16 1 0 multTable = Some 2 /\
  matrix_get Byte 16 16 1 1 multTable = Some 1 /\
  matrix_get Byte 16 16 1 2 multTable = Some 4 /\
  matrix_get Byte 16 16 1 3 multTable = Some 7 /\
  matrix_get Byte 16 16 1 4 multTable = Some 14 /\
  matrix_get Byte 16 16 1 5 multTable = Some 13 /\
  matrix_get Byte 16 16 1 6 multTable = Some 8 /\
  matrix_get Byte 16 16 1 7 multTable = Some 11 /\
  matrix_get Byte 16 16 1 8 multTable = Some 9 /\
  matrix_get Byte 16 16 1 9 multTable = Some 10 /\
  matrix_get Byte 16 16 1 10 multTable = Some 15 /\
  matrix_get Byte 16 16 1 11 multTable = Some 12 /\
  matrix_get Byte 16 16 1 12 multTable = Some 5 /\
  matrix_get Byte 16 16 1 13 multTable = Some 6 /\
  matrix_get Byte 16 16 1 14 multTable = Some 3 /\
  matrix_get Byte 16 16 1 15 multTable = Some 0 /\
  matrix_get Byte 16 16 2 0 multTable = Some 4 /\
  matrix_get Byte 16 16 2 1 multTable = Some 7 /\
  matrix_get Byte 16 16 2 2 multTable = Some 2 /\
  matrix_get Byte 16 16 2 3 multTable = Some 1 /\
  matrix_get Byte 16 16 2 4 multTable = Some 8 /\
  matrix_get Byte 16 16 2 5 multTable = Some 11 /\
  matrix_get Byte 16 16 2 6 multTable = Some 14 /\
  matrix_get Byte 16 16 2 7 multTable = Some 13 /\
  matrix_get Byte 16 16 2 8 multTable = Some 15 /\
  matrix_get Byte 16 16 2 9 multTable = Some 12 /\
  matrix_get Byte 16 16 2 10 multTable = Some 9 /\
  matrix_get Byte 16 16 2 11 multTable = Some 10 /\
  matrix_get Byte 16 16 2 12 multTable = Some 3 /\
  matrix_get Byte 16 16 2 13 multTable = Some 0 /\
  matrix_get Byte 16 16 2 14 multTable = Some 5 /\
  matrix_get Byte 16 16 2 15 multTable = Some 6 /\
  matrix_get Byte 16 16 3 0 multTable = Some 6 /\
  matrix_get Byte 16 16 3 1 multTable = Some 5 /\
  matrix_get Byte 16 16 3 2 multTable = Some 0 /\
  matrix_get Byte 16 16 3 3 multTable = Some 3 /\
  matrix_get Byte 16 16 3 4 multTable = Some 10 /\
  matrix_get Byte 16 16 3 5 multTable = Some 9 /\
  matrix_get Byte 16 16 3 6 multTable = Some 12 /\
  matrix_get Byte 16 16 3 7 multTable = Some 15 /\
  matrix_get Byte 16 16 3 8 multTable = Some 13 /\
  matrix_get Byte 16 16 3 9 multTable = Some 14 /\
  matrix_get Byte 16 16 3 10 multTable = Some 11 /\
  matrix_get Byte 16 16 3 11 multTable = Some 8 /\
  matrix_get Byte 16 16 3 12 multTable = Some 1 /\
  matrix_get Byte 16 16 3 13 multTable = Some 2 /\
  matrix_get Byte 16 16 3 14 multTable = Some 7 /\
  matrix_get Byte 16 16 3 15 multTable = Some 4 /\
  matrix_get Byte 16 16 4 0 multTable = Some 8 /\
  matrix_get Byte 16 16 4 1 multTable = Some 11 /\
  matrix_get Byte 16 16 4 2 multTable = Some 14 /\
  matrix_get Byte 16 16 4 3 multTable = Some 13 /\
  matrix_get Byte 16 16 4 4 multTable = Some 4 /\
  matrix_get Byte 16 16 4 5 multTable = Some 7 /\
  matrix_get Byte 16 16 4 6 multTable = Some 2 /\
  matrix_get Byte 16 16 4 7 multTable = Some 1 /\
  matrix_get Byte 16 16 4 8 multTable = Some 3 /\
  matrix_get Byte 16 16 4 9 multTable = Some 0 /\
  matrix_get Byte 16 16 4 10 multTable = Some 5 /\
  matrix_get Byte 16 16 4 11 multTable = Some 6 /\
  matrix_get Byte 16 16 4 12 multTable = Some 15 /\
  matrix_get Byte 16 16 4 13 multTable = Some 12 /\
  matrix_get Byte 16 16 4 14 multTable = Some 9 /\
  matrix_get Byte 16 16 4 15 multTable = Some 10 /\
  matrix_get Byte 16 16 5 0 multTable = Some 10 /\
  matrix_get Byte 16 16 5 1 multTable = Some 9 /\
  matrix_get Byte 16 16 5 2 multTable = Some 12 /\
  matrix_get Byte 16 16 5 3 multTable = Some 15 /\
  matrix_get Byte 16 16 5 4 multTable = Some 6 /\
  matrix_get Byte 16 16 5 5 multTable = Some 5 /\
  matrix_get Byte 16 16 5 6 multTable = Some 0 /\
  matrix_get Byte 16 16 5 7 multTable = Some 3 /\
  matrix_get Byte 16 16 5 8 multTable = Some 1 /\
  matrix_get Byte 16 16 5 9 multTable = Some 2 /\
  matrix_get Byte 16 16 5 10 multTable = Some 7 /\
  matrix_get Byte 16 16 5 11 multTable = Some 4 /\
  matrix_get Byte 16 16 5 12 multTable = Some 13 /\
  matrix_get Byte 16 16 5 13 multTable = Some 14 /\
  matrix_get Byte 16 16 5 14 multTable = Some 11 /\
  matrix_get Byte 16 16 5 15 multTable = Some 8 /\
  matrix_get Byte 16 16 6 0 multTable = Some 12 /\
  matrix_get Byte 16 16 6 1 multTable = Some 15 /\
  matrix_get Byte 16 16 6 2 multTable = Some 10 /\
  matrix_get Byte 16 16 6 3 multTable = Some 9 /\
  matrix_get Byte 16 16 6 4 multTable = Some 0 /\
  matrix_get Byte 16 16 6 5 multTable = Some 3 /\
  matrix_get Byte 16 16 6 6 multTable = Some 6 /\
  matrix_get Byte 16 16 6 7 multTable = Some 5 /\
  matrix_get Byte 16 16 6 8 multTable = Some 7 /\
  matrix_get Byte 16 16 6 9 multTable = Some 4 /\
  matrix_get Byte 16 16 6 10 multTable = Some 1 /\
  matrix_get Byte 16 16 6 11 multTable = Some 2 /\
  matrix_get Byte 16 16 6 12 multTable = Some 11 /\
  matrix_get Byte 16 16 6 13 multTable = Some 8 /\
  matrix_get Byte 16 16 6 14 multTable = Some 13 /\
  matrix_get Byte 16 16 6 15 multTable = Some 14 /\
  matrix_get Byte 16 16 7 0 multTable = Some 14 /\
  matrix_get Byte 16 16 7 1 multTable = Some 13 /\
  matrix_get Byte 16 16 7 2 multTable = Some 8 /\
  matrix_get Byte 16 16 7 3 multTable = Some 11 /\
  matrix_get Byte 16 16 7 4 multTable = Some 2 /\
  matrix_get Byte 16 16 7 5 multTable = Some 1 /\
  matrix_get Byte 16 16 7 6 multTable = Some 4 /\
  matrix_get Byte 16 16 7 7 multTable = Some 7 /\
  matrix_get Byte 16 16 7 8 multTable = Some 5 /\
  matrix_get Byte 16 16 7 9 multTable = Some 6 /\
  matrix_get Byte 16 16 7 10 multTable = Some 3 /\
  matrix_get Byte 16 16 7 11 multTable = Some 0 /\
  matrix_get Byte 16 16 7 12 multTable = Some 9 /\
  matrix_get Byte 16 16 7 13 multTable = Some 10 /\
  matrix_get Byte 16 16 7 14 multTable = Some 15 /\
  matrix_get Byte 16 16 7 15 multTable = Some 12 /\
  matrix_get Byte 16 16 8 0 multTable = Some 3 /\
  matrix_get Byte 16 16 8 1 multTable = Some 0 /\
  matrix_get Byte 16 16 8 2 multTable = Some 5 /\
  matrix_get Byte 16 16 8 3 multTable = Some 6 /\
  matrix_get Byte 16 16 8 4 multTable = Some 15 /\
  matrix_get Byte 16 16 8 5 multTable = Some 12 /\
  matrix_get Byte 16 16 8 6 multTable = Some 9 /\
  matrix_get Byte 16 16 8 7 multTable = Some 10 /\
  matrix_get Byte 16 16 8 8 multTable = Some 8 /\
  matrix_get Byte 16 16 8 9 multTable = Some 11 /\
  matrix_get Byte 16 16 8 10 multTable = Some 14 /\
  matrix_get Byte 16 16 8 11 multTable = Some 13 /\
  matrix_get Byte 16 16 8 12 multTable = Some 4 /\
  matrix_get Byte 16 16 8 13 multTable = Some 7 /\
  matrix_get Byte 16 16 8 14 multTable = Some 2 /\
  matrix_get Byte 16 16 8 15 multTable = Some 1 /\
  matrix_get Byte 16 16 9 0 multTable = Some 1 /\
  matrix_get Byte 16 16 9 1 multTable = Some 2 /\
  matrix_get Byte 16 16 9 2 multTable = Some 7 /\
  matrix_get Byte 16 16 9 3 multTable = Some 4 /\
  matrix_get Byte 16 16 9 4 multTable = Some 13 /\
  matrix_get Byte 16 16 9 5 multTable = Some 14 /\
  matrix_get Byte 16 16 9 6 multTable = Some 11 /\
  matrix_get Byte 16 16 9 7 multTable = Some 8 /\
  matrix_get Byte 16 16 9 8 multTable = Some 10 /\
  matrix_get Byte 16 16 9 9 multTable = Some 9 /\
  matrix_get Byte 16 16 9 10 multTable = Some 12 /\
  matrix_get Byte 16 16 9 11 multTable = Some 15 /\
  matrix_get Byte 16 16 9 12 multTable = Some 6 /\
  matrix_get Byte 16 16 9 13 multTable = Some 5 /\
  matrix_get Byte 16 16 9 14 multTable = Some 0 /\
  matrix_get Byte 16 16 9 15 multTable = Some 3 /\
  matrix_get Byte 16 16 10 0 multTable = Some 7 /\
  matrix_get Byte 16 16 10 1 multTable = Some 4 /\
  matrix_get Byte 16 16 10 2 multTable = Some 1 /\
  matrix_get Byte 16 16 10 3 multTable = Some 2 /\
  matrix_get Byte 16 16 10 4 multTable = Some 11 /\
  matrix_get Byte 16 16 10 5 multTable = Some 8 /\
  matrix_get Byte 16 16 10 6 multTable = Some 13 /\
  matrix_get Byte 16 16 10 7 multTable = Some 14 /\
  matrix_get Byte 16 16 10 8 multTable = Some 12 /\
  matrix_get Byte 16 16 10 9 multTable = Some 15 /\
  matrix_get Byte 16 16 10 10 multTable = Some 10 /\
  matrix_get Byte 16 16 10 11 multTable = Some 9 /\
  matrix_get Byte 16 16 10 12 multTable = Some 0 /\
  matrix_get Byte 16 16 10 13 multTable = Some 3 /\
  matrix_get Byte 16 16 10 14 multTable = Some 6 /\
  matrix_get Byte 16 16 10 15 multTable = Some 5 /\
  matrix_get Byte 16 16 11 0 multTable = Some 5 /\
  matrix_get Byte 16 16 11 1 multTable = Some 6 /\
  matrix_get Byte 16 16 11 2 multTable = Some 3 /\
  matrix_get Byte 16 16 11 3 multTable = Some 0 /\
  matrix_get Byte 16 16 11 4 multTable = Some 9 /\
  matrix_get Byte 16 16 11 5 multTable = Some 10 /\
  matrix_get Byte 16 16 11 6 multTable = Some 15 /\
  matrix_get Byte 16 16 11 7 multTable = Some 12 /\
  matrix_get Byte 16 16 11 8 multTable = Some 14 /\
  matrix_get Byte 16 16 11 9 multTable = Some 13 /\
  matrix_get Byte 16 16 11 10 multTable = Some 8 /\
  matrix_get Byte 16 16 11 11 multTable = Some 11 /\
  matrix_get Byte 16 16 11 12 multTable = Some 2 /\
  matrix_get Byte 16 16 11 13 multTable = Some 1 /\
  matrix_get Byte 16 16 11 14 multTable = Some 4 /\
  matrix_get Byte 16 16 11 15 multTable = Some 7 /\
  matrix_get Byte 16 16 12 0 multTable = Some 11 /\
  matrix_get Byte 16 16 12 1 multTable = Some 8 /\
  matrix_get Byte 16 16 12 2 multTable = Some 13 /\
  matrix_get Byte 16 16 12 3 multTable = Some 14 /\
  matrix_get Byte 16 16 12 4 multTable = Some 7 /\
  matrix_get Byte 16 16 12 5 multTable = Some 4 /\
  matrix_get Byte 16 16 12 6 multTable = Some 1 /\
  matrix_get Byte 16 16 12 7 multTable = Some 2 /\
  matrix_get Byte 16 16 12 8 multTable = Some 0 /\
  matrix_get Byte 16 16 12 9 multTable = Some 3 /\
  matrix_get Byte 16 16 12 10 multTable = Some 6 /\
  matrix_get Byte 16 16 12 11 multTable = Some 5 /\
  matrix_get Byte 16 16 12 12 multTable = Some 12 /\
  matrix_get Byte 16 16 12 13 multTable = Some 15 /\
  matrix_get Byte 16 16 12 14 multTable = Some 10 /\
  matrix_get Byte 16 16 12 15 multTable = Some 9 /\
  matrix_get Byte 16 16 13 0 multTable = Some 9 /\
  matrix_get Byte 16 16 13 1 multTable = Some 10 /\
  matrix_get Byte 16 16 13 2 multTable = Some 15 /\
  matrix_get Byte 16 16 13 3 multTable = Some 12 /\
  matrix_get Byte 16 16 13 4 multTable = Some 5 /\
  matrix_get Byte 16 16 13 5 multTable = Some 6 /\
  matrix_get Byte 16 16 13 6 multTable = Some 3 /\
  matrix_get Byte 16 16 13 7 multTable = Some 0 /\
  matrix_get Byte 16 16 13 8 multTable = Some 2 /\
  matrix_get Byte 16 16 13 9 multTable = Some 1 /\
  matrix_get Byte 16 16 13 10 multTable = Some 4 /\
  matrix_get Byte 16 16 13 11 multTable = Some 7 /\
  matrix_get Byte 16 16 13 12 multTable = Some 14 /\
  matrix_get Byte 16 16 13 13 multTable = Some 13 /\
  matrix_get Byte 16 16 13 14 multTable = Some 8 /\
  matrix_get Byte 16 16 13 15 multTable = Some 11 /\
  matrix_get Byte 16 16 14 0 multTable = Some 15 /\
  matrix_get Byte 16 16 14 1 multTable = Some 12 /\
  matrix_get Byte 16 16 14 2 multTable = Some 9 /\
  matrix_get Byte 16 16 14 3 multTable = Some 10 /\
  matrix_get Byte 16 16 14 4 multTable = Some 3 /\
  matrix_get Byte 16 16 14 5 multTable = Some 0 /\
  matrix_get Byte 16 16 14 6 multTable = Some 5 /\
  matrix_get Byte 16 16 14 7 multTable = Some 6 /\
  matrix_get Byte 16 16 14 8 multTable = Some 4 /\
  matrix_get Byte 16 16 14 9 multTable = Some 7 /\
  matrix_get Byte 16 16 14 10 multTable = Some 2 /\
  matrix_get Byte 16 16 14 11 multTable = Some 1 /\
  matrix_get Byte 16 16 14 12 multTable = Some 8 /\
  matrix_get Byte 16 16 14 13 multTable = Some 11 /\
  matrix_get Byte 16 16 14 14 multTable = Some 14 /\
  matrix_get Byte 16 16 14 15 multTable = Some 13 /\
  matrix_get Byte 16 16 15 0 multTable = Some 13 /\
  matrix_get Byte 16 16 15 1 multTable = Some 14 /\
  matrix_get Byte 16 16 15 2 multTable = Some 11 /\
  matrix_get Byte 16 16 15 3 multTable = Some 8 /\
  matrix_get Byte 16 16 15 4 multTable = Some 1 /\
  matrix_get Byte 16 16 15 5 multTable = Some 2 /\
  matrix_get Byte 16 16 15 6 multTable = Some 7 /\
  matrix_get Byte 16 16 15 7 multTable = Some 4 /\
  matrix_get Byte 16 16 15 8 multTable = Some 6 /\
  matrix_get Byte 16 16 15 9 multTable = Some 5 /\
  matrix_get Byte 16 16 15 10 multTable = Some 0 /\
  matrix_get Byte 16 16 15 11 multTable = Some 3 /\
  matrix_get Byte 16 16 15 12 multTable = Some 10 /\
  matrix_get Byte 16 16 15 13 multTable = Some 9 /\
  matrix_get Byte 16 16 15 14 multTable = Some 12 /\
  matrix_get Byte 16 16 15 15 multTable = Some 15
.
